/**********************************************************************
* Filename: Reserva.java
* Created: 2013/05/30
* @author Fernando Brito e Abreu
**********************************************************************/
package org.quasar.airNova.businessLayer;

import org.quasar.airNova.persistenceLayer.Database;

import java.util.Set;
import java.util.TreeSet;
import java.util.SortedSet;

public class Reserva
{
	
	/***********************************************************
	* @return all instances of class Reserva
	***********************************************************/
	public static Set<Reserva> allInstances()
	{
		return Database.allInstances(Reserva.class);
	}
	
	private CartaoCredito cartaoCredito;
	private Cliente cliente;
	private int n_reserva;
	private EstadoPagamento pagamento;
	
	/**********************************************************************
	* Default constructor
	**********************************************************************/
	public Reserva()
	{
	}
	
	/**********************************************************************
	* Parameterized constructor
	* @param cartaoCredito the cartaoCredito to initialize
	* @param cliente the cliente to initialize
	* @param n_reserva the n_reserva to initialize
	* @param pagamento the pagamento to initialize
	**********************************************************************/
	public Reserva(CartaoCredito cartaoCredito, Cliente cliente, int n_reserva, EstadoPagamento pagamento)
	{
		this.cartaoCredito = cartaoCredito;
		this.cliente = cliente;
		this.n_reserva = n_reserva;
		this.pagamento = pagamento;
	}
	
	/**********************************************************************
	* ONE2MANY getter for Reserva[*] <-> CartaoCredito[1]
	* @return the cartaoCredito of the reserva
	**********************************************************************/
	public CartaoCredito cartaoCredito()
	{
		return cartaoCredito;
	}
	
	/**********************************************************************
	* ONE2MANY setter for Reserva[*] <-> CartaoCredito[1]
	* @param cartaoCredito the cartaoCredito to set
	**********************************************************************/
	public void setCartaoCredito(CartaoCredito cartaoCredito)
	{
		this.cartaoCredito = cartaoCredito;
	}
	
	/**********************************************************************
	* ONE2MANY getter for Reserva[*] <-> Cliente[1]
	* @return the cliente of the reserva
	**********************************************************************/
	public Cliente cliente()
	{
		return cliente;
	}
	
	/**********************************************************************
	* ONE2MANY setter for Reserva[*] <-> Cliente[1]
	* @param cliente the cliente to set
	**********************************************************************/
	public void setCliente(Cliente cliente)
	{
		this.cliente = cliente;
	}
	
	/**********************************************************************
	* Standard attribute getter
	* @return the n_reserva of the reserva
	**********************************************************************/
	public int n_reserva()
	{
		return n_reserva;
	}
	
	/**********************************************************************
	* Standard attribute setter
	* @param n_reserva the n_reserva to set
	**********************************************************************/
	public void setN_reserva(int n_reserva)
	{
		this.n_reserva = n_reserva;
	}
	
	/**********************************************************************
	* Standard attribute getter
	* @return the pagamento of the reserva
	**********************************************************************/
	public EstadoPagamento pagamento()
	{
		return pagamento;
	}
	
	/**********************************************************************
	* Standard attribute setter
	* @param pagamento the pagamento to set
	**********************************************************************/
	public void setPagamento(EstadoPagamento pagamento)
	{
		this.pagamento = pagamento;
	}
	
	/**********************************************************************
	* ONE2MANY getter for Reserva[0..1] <-> Bilhete[*] ordered
	* @return the bilhetes of the reserva
	**********************************************************************/
	public SortedSet<Bilhete> bilhetes()
	{
		SortedSet<Bilhete> result = new TreeSet<Bilhete>();
		for (Bilhete x : Bilhete.allInstances())
			if (x.reserva()  ==  this)
				result.add(x);
		return result;
	}
	
	/**********************************************************************
	* ONE2MANY multiple setter for Reserva[0..1] <-> Bilhete[*] ordered
	* @param bilhetes the bilhetes to set
	**********************************************************************/
	public void setBilhetes(SortedSet<Bilhete> bilhetes)
	{
		for (Bilhete x : bilhetes)
			x.setReserva(this);
	}
	
	/**********************************************************************
	* ONE2MANY single setter for Reserva[0..1] <-> Bilhete[*] ordered
	* @param bilhete the bilhete to add
	**********************************************************************/
	public void addBilhetes(Bilhete bilhete)
	{
		bilhete.setReserva(this);
	}
	
	/**********************************************************************
	* User-defined operation specified in SOIL/OCL
	* @param b the b to set
	* @param cd the cd to set
	* @param r the r to set
	**********************************************************************/
	public void CancelarBilhete(Bilhete b, CalendarDate cd, Realizacao r)
	{
		//	TODO
	}
	
	//	PRE-CONDITIONS (TODO)
	/*
	pre DataDeCancelamentoValida
		cd.isBefore(b.realizacao.ocorre_em)
	
	*/
	
	//	POST-CONDITIONS (TODO)
	/*
	post BilheteCancelado
		self.bilhetes->excludes(b)
	
	*/
	
	/**********************************************************************
	* User-defined operation specified in SOIL/OCL
	* @param v the v to set
	* @param cd the cd to set
	* @param lugar the lugar to set
	**********************************************************************/
	public void ComprarBilhete(Voo v, CalendarDate cd, int lugar)
	{
		//	TODO
	}
	
	//	PRE-CONDITIONS (TODO)
	/*
	pre CartaoValido
		(self.cartaoCredito.data_expira.isAfter(self.cartaoCredito.data_expira.now) and (self.cartaoCredito.numero > 0))
	
	pre VerificaLugarDesocupado
		self.bilhetes->forAll(bb : Bilhete | (lugar <> bb.lugar))
	
	pre LugaresDisponiveis
		v.realizacao->collectNested($e : Realizacao | $e.aviao)->collectNested($e : Aviao | $e.capacidade)->flatten->forAll(c1 : Capacidade | (c1.Lotacao() > lugar))
	
	*/
	
	//	POST-CONDITIONS (TODO)
	/*
	post ReservaFeitaBilheteComprado
		self.bilhetes->exists(bb : Bilhete | (lugar = bb.lugar))
	
	*/
	
	/**********************************************************************
	* Object serializer
	**********************************************************************/
	public String toString()
	{
		return "Reserva [cartaoCredito=" + cartaoCredito + ", cliente=" + cliente + ", n_reserva=" + n_reserva + ", pagamento=" + pagamento + "]";
	}
	
	//	-------------------------------------------------------------------------------
	//	INVARIANTS (TODO)
	/*
	inv osClientesTemQueSerIguais
		(self.cartaoCredito.possuidor = self.cliente)
	
	inv umaReservaTemDiferentesBilhetes
		self.bilhetes->collectNested($e : Bilhete | $e.realizacao)->collectNested($e : Realizacao | $e.realiza_se)->forAll(v : Voo | v.realizacao->collectNested($e : Realizacao | $e.bilhetes)->flatten->forAll(b1 : Bilhete, b2 : Bilhete | ((b1 <> b2) implies if (b1.classe = b2.classe) then (b1.lugar <> b2.lugar) else (b1.classe <> b2.classe) endif)))
	
	inv primeirasReservasComMenorClasse
		(self.bilhetes->collectNested($e : Bilhete | $e.classe)->first.tipo = TipoClasse::turistica)
	
	*/
}
